package com.googlecode.kipler.satisfiability.reasoner;

import com.googlecode.kipler.syntax.formula.Formula;

public interface SATReasoner extends Reasoner {
	/**
	 * 
	 * @return true if the knowledge base is satisfiable.
	 * @throws Exception
	 */
	public boolean isSatisfiable() throws Exception;

	/**
	 * @param formula
	 * @return true if the given formula can logically be inferred from the
	 *         knowledge base.
	 * @throws Exception
	 */
	public boolean isLogicalConsequence(Formula formula) throws Exception;
}
